NIL 
EVAL-AWAITS 
NIL 1 2
1 C = T;3 4
2 ¬C = T;AXIOM
3 clear(C,S0)⊃C = T;5 38
4 clear(C,S0);AXIOM
5 ¬clear(C,R(puton(C,T),S0));7 32
7 clear(C,R(puton(C,T),S0))⊃B = T;30 10
10 clear(B,S0)∧clear(C,R(puton(C,T),S0))⊃B = T;11 38
11 ¬(clear(B,R(puton(C,T),S0))∧clear(C,R(puton(C,T),S0)));13 40
13 ¬on(B,C,R(puton(x,C),R(puton(C,T),S0)));15 16
15 on(B,C,R(puton(x,C),R(puton(C,T),S0)))⊃A = B;17 18
16 ¬A = B;AXIOM
17 ¬on(B,C,R(puton(A,B),R(puton(x,C),R(puton(C,T),S0))));19 20
18 on(x,y,s)⊃z = x∨on(x,y,R(puton(z,u),s));AXIOM
19 on(B,C,R(puton(A,B),R(puton(x,C),R(puton(C,T),S0))))⊃T = A;21 22
20 ¬T = A;AXIOM
21 on(y,A,S0)∧on(B,C,R(puton(A,B),R(puton(x,C),R(puton(y,T),S0))))⊃T = A;23 24
22 on(C,A,S0);AXIOM
23 on(y,x,u)⊃z = x∨clear(x,R(puton(y,z),u));AXIOM
24 ¬(on(B,C,R(puton(A,B),R(puton(y,C),R(puton(x,T),S0))))∧clear(A,R(puton(x,T),S0)));25 26
25 on(B,C,R(puton(A,B),R(puton(y,C),R(puton(x,T),S0))))∧clear(A,R(puton(x,T),S0))⊃A = C;27 38
26 ¬A = C;AXIOM
27 ¬(on(B,C,R(puton(A,B),R(puton(x,C),R(puton(y,T),S0))))∧clear(A,R(puton(x,C),R(puton(y,T),S0))));29 30
29 ¬(on(B,C,R(puton(A,B),R(puton(x,C),R(puton(y,T),z))))∧(clear(B,z)∧clear(A,R(puton(x,C),R(puton(y,T),z)))));31~
 32
30 clear(B,S0);AXIOM
31 on(B,C,R(puton(A,B),R(puton(y,C),R(puton(z,x),u))))∧(clear(B,u)∧clear(A,R(puton(y,C),R(puton(z,x),u))))⊃B = x~
;33 38
32 ¬B = T;AXIOM
33 ¬(on(B,C,R(puton(A,B),R(puton(x,C),y)))∧(clear(B,y)∧clear(A,R(puton(x,C),y))));35 36
35 on(B,C,R(puton(A,B),R(puton(y,x),z)))∧(clear(B,z)∧clear(A,R(puton(y,x),z)))⊃B = x;37 38
36 ¬B = C;AXIOM
37 ¬(on(B,C,R(puton(A,B),x))∧(clear(A,x)∧clear(B,x)));39 40
38 clear(x,u)⊃x = z∨clear(x,R(puton(y,z),u));AXIOM
39 ¬(on(A,B,x)∧on(B,C,x));THM
40 clear(x,z)∧clear(y,z)⊃on(x,y,R(puton(x,y),z));AXIOM
NIL 
EVAL-AWAITS